chore: replace haveI/letI with have/let in tactic proofs of propositions#41615
chore: replace haveI/letI with have/let in tactic proofs of propositions#41615kbuzzard wants to merge 3 commits into
Conversation
The `haveI`/`letI` tactics differ from `have`/`let` only in that they inline
their value into the proof term rather than binding it. In a tactic proof of a
proposition this difference is invisible by proof irrelevance, so `have`/`let`
should be used instead.
This applies the fixes flagged by the `linter.style.haveILetI` linter across
Mathlib, Archive and Counterexamples: 2649 sites in 964 files, each an
elaborator-certified use of the `haveI`/`letI` *tactic* whose main goal is a
proposition. Term-mode `haveI`/`letI` and uses whose goal is data are left
untouched.
One site (`CategoryTheory/Galois/Basic.lean`) additionally needed an explicit
universe annotation `FintypeCat.{w}`, because the `have` tactic checks the
declared type's universe eagerly whereas `haveI`, elaborated in term mode,
defers it until the value pins it down.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
!bench |
|
Benchmark results for 766ff5c against 32ea179 are in. No significant results found. @kbuzzard Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
Medium changes (1🟥)
Small changes (1🟥) 1 hidden |
github-actions
Bot
added
the
merge-conflict
|
|
||
| theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (hp_gt_20 : p > 20) : | ||
| ∃ n : ℕ, p ∣ n ^ 2 + 1 ∧ (p : ℝ) > 2 * n + sqrt (2 * n) := by | ||
| haveI := Fact.mk hpp |
There was a problem hiding this comment.
But for things like this, isnt inlining preferable?
There was a problem hiding this comment.
Perhaps, but that is not the job of this PR. The job of this PR is to follow the convention of no haveI in tactic proofs. The issue you are raising is already present in mathlib master.
There was a problem hiding this comment.
Ok good then. The convention of not using haveI in tactic proofs isnt in the style guide. I think maybe it would good to mention it explicitly there also (maybe that will also help AI to not use it as much).
…fixes # Conflicts: # Mathlib/RingTheory/LaurentSeries.lean # Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean # Mathlib/RingTheory/UniqueFactorizationDomain/GCDMonoid.lean # Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicative.lean # Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean
github-actions
Bot
removed
the
merge-conflict
PR summary 115c0636d8Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
!radar |
|
Benchmark results for 115c063 against 4efb186 are in. No significant results found. @kbuzzard
Medium changes (1🟥)
|
3 participants
My understanding is that we should be using
have/letrather thanhaveI/letIin tactic proofs. I noticed that AI was getting this wrong and I suspect that it's because we're getting this wrong in mathlib a lot (possibly becausehaveImeant something different in Lean 3), and AI is training on mathlib.Does this matter? In my experience the reaction of the community will be one of two things:
I got Claude to write a linter to check for this, and it's #41562 . It's completely vibe-coded and I cannot vouch for any of it.
The result, when running it on mathlib, is the diff in this PR. In particular, we're getting it wrong a lot.
I was intrigued to find out how often we're making this mistake in mathlib, and it probably took me about 10 minutes of my own time to get AI to write the linter and run it on mathlib. I will not mark this PR as AI-generated because it was generated by a linter. The linter itself was AI generated. It is not clear to me whether we should be merging this PR without merging the linter, and the linter will need careful human review, but I figured I would give the community the option to merge this PR anyway.